Nuprl Lemma : list_n_properties
2,24
postcript
pdf
A
:Type,
n
:
,
as
:
A
List(
n
). ||
as
|| =
n
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
A
List(
n
)
Lemmas
list
n
wf
origin
A:Type, n:
, as:A List(n). ||as|| = n A:Type, n:, as:A List(n). ||as|| = n 
Tx:A. B(x)